One approach to analysing program code is to inline function calls, which means that the implementation of a function is copied into the program every time that function is called. This results in a code size that is exponential in the number of nested function calls.
Many industrial-strength source code analysers face similar challenges: 1) it is generally difficult to build a complete monolithic representation of the software as it is often too large to fit into memory; 2) source code of some pieces of the software may not be available, such as library functions; 3) noise created by false positives may render the analysis unusable and 4) providing developers with feasible inter-procedural counter-examples is still an issue.
Any discussion of documents, acts, materials, devices, articles or the like which has been included in the present specification is not to be taken as an admission that any or all of these matters form part of the prior art base or were common general knowledge in the field relevant to the present disclosure as it existed before the priority date of each claim of this application.